Nestan Tsiskaridze, University of California, Santa Barbara The modern world critically depends on the security and safety of software. We seek to ensure customer confidence and protect privacy, intellectual property, and national security. As threats to software security have become more sophisticated, so too have the techniques developed to ensure security. This talk focuses on novel opportunities to automate bug detection and security exploit generation provided by advances in symbolic execution and automated constraint solving. It discusses how symbolic execution can benefit from novel techniques in Satisfiability Modulo Theories (SMT), a subfield of automated theorem proving that in the past 10 years has revolutionized the discipline. The talk presents a recent highly successful application of SMT solvers in support of the security analysis of Web applications and how these new capabilities open opportunities for automating such analysis beyond the Web. This is a joint work with Clark Barrett (NYU/Stanford University), Morgan Deters (NYU), Tianyi Liang (The University of Iowa), Andrew Reynolds (The University of Iowa/EPFL), and Cesare Tinelli (The University of Iowa). Sign up to find out more about Enigma conferences: https://www.usenix.org/conference/enigma2017#signup Watch all Enigma 2017 videos at: http://enigma.usenix.org/youtube

Source: https://www.youtube.com/watch?v=wLlnKu4HmaU
Uploader: USENIX Enigma Conference
Upload date: 2017-03-06

plus-circle Add Review

comment

Reviews